COM: quot 1 summary

COM: quot 1 intro

STM: quotient wf

STM: quotient qinc

STM: type inj wf for quot

STM: quot elim

STM: all quot elim

STM: dec iff ex bvfun

STM: decidable quotient equal

COM: quot 1 end